Verification of event-driven software systems using the specification language of cooperating automata objects
Annotation
The CIAO (Cooperative Interaction Automata Objects) specification language is intended to describe the behavior of distributed and parallel event-driven systems. This class of systems includes various software and hardware systems for control, monitoring, data collection, and processing. The ability to verify compliance with requirements is desirable competitive advantage for such systems. The CIAO language extends the concept of state machines of the UML (Unified Modeling Language) with the possibility of cooperative interaction of several automata through strictly defined interfaces. The cooperative interaction of automatа objects is defined by a link scheme that defines how the provided and required interfaces of different automatа objects are connected. Thus, the behavior of the system as a whole could be described as a set of execution protocols, each of which is a sequence of interface calls, possibly with guard conditions. We represent a set of protocols using a semantic graph in which all possible paths from the initial nodes to the final nodes define sequences of interface method calls. Because the interfaces are strictly defined in advance by the connection scheme, it is possible to construct a semantic graph automatically according to a given system of interacting automaton objects. To verify the system behavior, one only has to check if each path in the semantic graph does satisfy the requirements. System requirements are formally described using conditional regular expressions that define patterns of acceptable and forbidden behavior. This article proposes methods and algorithms that allow you to check the compliance of programs in the CIAO language with the requirements automatically and, thereby, check the semantics of the developed program. The proposed method narrows the specification formalism to the class of regular languages and the programming language to a language with a simple and predefined structure. In many practical cases, this is sufficient for effective verification.
Keywords
Постоянный URL
Articles in current issue
- Determination of the action type of hydrate formationinhibitors by their infrared spectra
- Application of Raman spectroscopy to study the inactivation process of bacterial microorganisms
- Numerical study of the effect of methemoglobin concentration in the blood on the absorption of light by human skin.
- Low-temperature cell for IR Fourier spectrometric investigation of hydrocarbon substances
- Peculiarities of growing Ga1–xInxAs solid solutions on GaAs substrates in the field of a temperature gradient through a thin gas zone
- An enhanced AES-GCM based security protocol for securing the IoT communication
- Attacks based on malicious perturbations on image processing systems and defense methods against them
- Brain MRT image super resolution using discrete cosine transform and convolutional neural network
- Text augmentation preserving persona speech style and vocabulary
- Intelligent adaptive testing system
- Neural network-based method for visual recognition of driver’s voice commands using attention mechanism
- Brain tumour segmentation in MRI using fuzzy deformable fusion model with Dolphin-SCA
- Optimization of human tracking systems in virtual reality based on a neural network approach
- Errors in the demodulation algorithm with a generated carrier phase introduted by the low-pass filter
- Modeling of the process of spherical form correction for rotors of electrostatically suspended gyros
- Method of spatial multiplexing in multi-antenna communication systems
- Modeling and simulation of heat exchanger with strong dependence of oil viscosity on temperature
- Approach to the generalized parameters formation of the complex technical systems technical condition using neural network structures
- Numerical simulation of gas dynamics during operation of a wide-range rocket nozzle with a porous insert
- The exact solution of a shock wave reflection problem from a wall shielded by a gas suspension layer
- Adaptive observer for state variables of a time-varying nonlinear system with unknown constant parameters and delayed measurements
- RuLegalNER: a new dataset for Russian legal named entities recognition